\begin{tabbing}
$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), ${\it as}$:($T$ List).
\\[0ex]($\exists$$a$:$T$. (($a$ $\in$ ${\it as}$) \& ($\uparrow$$P$($a$))))
\\[0ex]$\Rightarrow$ \=((hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ $T$)\+
\\[0ex]c$\wedge$ ((hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ ${\it as}$) \& ($\uparrow$$P$(hd(filter($\lambda$$a$.$P$($a$);${\it as}$))))))
\-
\end{tabbing}